nLab Peter Selinger

• personal webpage

• institute page

Selected writings

Early consideration of quantum programming languages (QPL):

• Peter Selinger, Towards a quantum programming language, Mathematical Structures in Computer Science 14(4):527–586, 2004 (doi:10.1017/S0960129504004256, pdf, web)

via quantum lambda-calculus invoking linear types:

• Peter Selinger, Benoît Valiron, A lambda calculus for quantum computation with classical control, Proc. of TLCA 2005 $[$arXiv:cs/0404056, doi:10.1007/11417170_26$]$

• Peter Selinger, Benoît Valiron, Quantum Lambda Calculus, in: Semantic Techniques in Quantum Computation, Cambridge University Press (2009) 135-172 $[$doi:10.1017/CBO9781139193313.005, pdf$]$

[Selinger (2016):] When the QPL workshop series was first founded, it was called “Quantum Programming Languages”. One year I wasn’t participating, and while I wasn’t looking they changed the name to “Quantum Physics and Logic” — same acronym!

Back in those days in the early 21st century we were actually trying to do programming languages for quantum computing $[$Selinger & Valiron 2004$]$, but the sad thing is: In those days nobody really cared. $[...]$

Now it’s 15 years later and several of these parameters have changed: There has been a renewed interest, from government agencies and also from companies who are actually building quantum computers. $[...]$.

So now people are working on quantum programming languages again.

then via Quipper:

• Alexander Green, Peter LeFanu Lumsdaine, Neil Ross, Peter Selinger, Benoît Valiron, Quipper: A Scalable Quantum Programming Language, ACM SIGPLAN Notices 48(6):333-342, 2013 (arXiv:1304.3390)

• Alexander Green, Peter LeFanu Lumsdaine, Neil Ross, Peter Selinger, Benoît Valiron, An Introduction to Quantum Programming in Quipper, Lecture Notes in Computer Science 7948:110-124, Springer, 2013 (arXiv:1304.5485)

• Jonathan Smith, Neil Ross, Peter Selinger, Benoît Valiron, Quipper: Concrete Resource Estimation in Quantum Algorithms, QAPL 2014 (arXiv:1412.0625)

• Peter Selinger, The Quipper Language (web)

• Peter Selinger, Introduction to Quipper, talk at QPL2016 (2016) [video]

On self-dual objects in star-autonomous categories and their relation to inner products and to dagger-structure:

• Peter Selinger, Autonomous categories in which $A \simeq A^\ast$, talk at QPL 2012 (pdf)

On string diagram-calculus for monoidal categories:

• Peter Selinger, A survey of graphical languages for monoidal categories, in: Bob Coecke (ed.) New Structures for Physics, Lecture Notes in Physics, vol 813. Springer, Berlin, Heidelberg (2010) (arXiv:0908.334, doi:10.1007/978-3-642-12821-9_4)

On finite-dimensional Hilbert spaces as a dagger-compact category:

• Peter Selinger, Finite dimensional Hilbert spaces are complete for dagger compact closed categories, Logical Methods in Computer Science, 8 3 (2012) lmcs:1086 [arXiv:1207.6972, doi:10.2168/LMCS-8(3:6)2012]

Exposition of the general idea of quantum programming languages for classically controlled quantum computation with an eye towards the Quipper-language:

• Benoît Valiron, Neil J. Ross, Peter Selinger, D. Scott Alexander, Jonathan M. Smith, Programming the quantum future, Communications of the ACM 58 8 (2015) 52–61 [doi:10.1145/2699415, pdf, web, promo vid:YT]

On categorical semantics for Quipper:

• Francisco Rios, Peter Selinger, A Categorical Model for a Quantum Circuit Description Language, EPTCS 266 (2018) 164-178 [arXiv:1706.02630, doi:10.4204/EPTCS.266.11]

On quantum programming via dependent linear type theory:

• Peng Fu, Kohei Kishida, Peter Selinger, Linear Dependent Type Theory for Quantum Programming Languages, LICS ‘20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer ScienceJuly 2020 Pages 440–453 (arXiv:2004.13472, doi:10.1145/3373718.3394765, pdf, video)

• Peng Fu, Kohei Kishida, Neil Ross, Peter Selinger, A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper, in I. Lanese, M. Rawski (eds.) Reversible Computation RC 2020. Lecture Notes in Computer Science, vol 12227 (arXiv:2005.08396, doi:10.1007/978-3-030-52482-1_9)

On the Agda proof assistant:

• Peter Selinger, Lectures on Agda (2021) [web]

On dependent linear type theory and categorical semantics for versions of “Quipper”:

• Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger, A biset-enriched categorical model for Proto-Quipper with dynamic lifting [arXiv:2204.13039]

• Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger, Proto-Quipper with dynamic lifting [arXiv:2204.13041]

category: people